*****∧I INDUCTION1;

1 (∀x.(ATOM x⊃∀u.LIST FLAT(x,u))∧∀x.((¬ATOM x∧(∀u.LIST FLAT(CAR x,u)∧∀u.LIST FLAT(CDR x,u)))⊃∀u.LIST FLAT(x,u)))%
⊃∀x u.LIST FLAT(x,u)  

*****∀E FLAT x,u;

2 FLAT(x,u)=IF ATOM x THEN CONS(x,u) ELSE FLAT(CAR x,FLAT(CDR x,u))  

*****DISTRIB;

3 FLAT(x,u)=IF ATOM x THEN CONS(x,u) ELSE FLAT(CAR x,FLAT(CDR x,u))≡IF ATOM x THEN FLAT(x,u)=CONS(x,u) ELSE FLAT%
(x,u)=FLAT(CAR x,FLAT(CDR x,u))  

*****ASSUME ATOM x;

4 ATOM x  (4)

*****TAUT FLAT(x,u)=CONS(x,u) ↑↑↑:↑;

5 FLAT(x,u)=CONS(x,u)  (4)

*****∀E CONS2 x,u;

6 LIST CONS(x,u)  

*****TAUTEQ LIST FLAT(x,u) ↑↑:↑;

7 LIST FLAT(x,u)  (4)

*****∀I ↑ u;

8 ∀u.LIST FLAT(x,u)  (4)

*****⊃I 4⊃↑;

9 ATOM x⊃∀u.LIST FLAT(x,u)  

*****∀I ↑ x;

10 ∀x.(ATOM x⊃∀u.LIST FLAT(x,u))  

*****ASSUME ¬ATOM x;

11 ¬ATOM x  (11)

*****TAUT FLAT(x,u)=FLAT(CAR x,FLAT(CDR x,u)) 2:3,↑;

12 FLAT(x,u)=FLAT(CAR x,FLAT(CDR x,u))  (11)

*****ASSUME ∀u.LIST FLAT(CAR x,u);

13 ∀u.LIST FLAT(CAR x,u)  (13)

*****ASSUME ∀u.LIST FLAT(CDR x,u);

14 ∀u.LIST FLAT(CDR x,u)  (14)

*****∀E ↑ u;

15 LIST FLAT(CDR x,u)  (14)

*****∀E ↑↑↑ FLAT(CDR x,u);

16 LIST FLAT(CDR x,u)⊃LIST FLAT(CAR x,FLAT(CDR x,u))  (13)

*****TAUTEQ LIST FLAT(x,u) 12,↑↑:↑;

17 LIST FLAT(x,u)  (11 13 14)

*****∀I ↑ u;

18 ∀u.LIST FLAT(x,u)  (11 13 14)

*****⊃I 14⊃↑;

19 ∀u.LIST FLAT(CDR x,u)⊃∀u.LIST FLAT(x,u)  (11 13)

*****⊃I 13⊃↑;

20 ∀u.LIST FLAT(CAR x,u)⊃(∀u.LIST FLAT(CDR x,u)⊃∀u.LIST FLAT(x,u))  (11)

*****⊃I 11⊃↑;

21 ¬ATOM x⊃(∀u.LIST FLAT(CAR x,u)⊃(∀u.LIST FLAT(CDR x,u)⊃∀u.LIST FLAT(x,u)))  

*****TAUT (¬ATOM x∧(∀u.LIST FLAT(CAR x,u)∧∀u.LIST FLAT(CDR x,u)))⊃∀u.LIST FLAT(x,u) ↑;

22 (¬ATOM x∧(∀u.LIST FLAT(CAR x,u)∧∀u.LIST FLAT(CDR x,u)))⊃∀u.LIST FLAT(x,u)  

*****∀I ↑ x;

23 ∀x.((¬ATOM x∧(∀u.LIST FLAT(CAR x,u)∧∀u.LIST FLAT(CDR x,u)))⊃∀u.LIST FLAT(x,u))  

*****TAUT ∀x u.LIST FLAT(x,u) 1,10,↑;

24 ∀x u.LIST FLAT(x,u)